#include <iostream>
#include <fstream>
#include <cstdlib>
#include "Sat.h"

using namespace std;

Sat::Sat(int nbVertex): evaluated(false), nbVertex(nbVertex), 
			problem(vector< vector<int> >()), cover(vector<int>()) 
{
  
}

Sat::Sat(Sat & s): evaluated(s.evaluated), nbVertex(s.nbVertex), 
		   problem(vector< vector<int> >(s.problem)), cover(vector<int>(s.cover)){}

Sat::Sat()
{
}
		    
Sat::~Sat()
{
}

void Sat::addClause(vector<int> v)
{
  problem.push_back(v);
}

vector<int> Sat::getCover()
{
  if (evaluated) 
    {
      return cover;
    } 
  else 
    {
      cerr << "Error : trying to get a solution of a non-evaluated SAT problem" << endl;
      return vector<int>();
    }
}

void Sat:: runMinisat() 
{
  system("./minisat_static in out");
  evaluated = true;
}

void Sat:: writeInfile() 
{
  ofstream out ("in", ios_base::out | ios_base::trunc);

  out << "p cnf "<< nbVertex << " " << problem.size() << endl; //p cnf <nb variables> <nb clauses>
  for (int i = 0; i < problem.size(); ++i)
    {
      for(int j = 0; j < problem[i].size(); ++j)
	{
	  out << problem[i][j];
	  out << " ";
	}
      out << "0\n";
    }
  out.close();
}

bool Sat::readOutfile()
{
  ifstream in ("out", ios_base::in);
  
  string sat;
  in >> sat;
  bool satisfiable = (sat == "SAT");
  
  int i;
  while(in.good())
    {
      in >> i;      
      if (i > 0)
	{
	  cover.push_back(i);
	}
    }
  in.close();
  
  return satisfiable;
}

